Hello World in Henk

Для рекурсивних монадичних скінченних програм використовується терм Morte/recursive, а для корекурсивних комонадичних нескінченних программ використовується терм Morte/corecursive. Все це відбувається в чистій лямбді, а саме Calculus of Constructions, елементарній мові з залежними типами та мінімальній ситемі доведення теорем, яку ше називаються одноаксіоматичною системою типів, так як вона містить лише один тип Пі.

$ cat Morte/recursive #IO/replicateM #Nat/Five (#IO/[>>=] #IO/data #Unit/@ #IO/getLine #IO/putLine)

Нагадуємо собі, що таке IO и [>>=] (в Хаскель еквіваленті), які постачаються з базовою біблиотекою Henk:

#IO/data : #String = #List #Nat

Сама вільна монада IO на Хаскель псевдокоді буде виглядати так:

data IO r = PutStrLn String (IO r) | GetLine (String -> IO r) | Return r (>>=) :: IO a -> (a -> IO b) -> IO b PutStrLn str io >>= f = PutStrLn str (io >>= f) GetLine k >>= f = GetLine (\str -> k str >>= f) Return r >>= f = f r

Компіляція (екстракт сертифікованої програми) в Erlang:

> om:extract("priv/normal/Morte").

Для запуску цієї монади нам потрібні індуктивні біндінги, тобто зовнішні ефекти у вигляді функцій, які ми передаємо як параметри в скомпільований терм Morte/recursive:

pure() -> fun(IO) -> IO end. getLine() -> fun(IO) -> fun(_) -> L = ch:list(io:get_line("> ")), ch:ap(IO,[L]) end end. putLine() -> fun(S) -> fun(IO) -> io:format(": "), io:put_chars(ch:unlist(S)), ch:ap(IO,[S]) end end. ma() -> ap('Morte':recursive(),[getLine(),putLine(),pure(),ch:nil()]).

Запускаємо:

> ch:ma(). > 1 : 1 > 2 : 2 > 3 : 3 > 4 : 4 > 5 : 5 #Fun

Ви щойно побачили найчистіший з аплікативних біндінгів в функціональних тотальних мовах програмування.